/*
 * Alloy Analyzer 4 -- Copyright (c) 2006-2008, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package edu.ut.ece382c.valloy.ast;

import java.util.List;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.JoinableList;
import edu.ut.ece382c.valloy.parser.Decl;
import static edu.ut.ece382c.valloy.ast.Type.EMPTY;

/**
 * Immutable; represents a quantified expression.
 *
 * It can have one of the following forms:
 *
 * <br>
 * <br>  ( all  a,b:t | formula )
 * <br>  ( no   a,b:t | formula )
 * <br>  ( lone a,b:t | formula )
 * <br>  ( one  a,b:t | formula )
 * <br>  ( some a,b:t | formula )
 * <br>  ( sum  a,b:t | integer expression )
 * <br>  { a,b:t | formula }
 * <br>  { a,b:t }
 * <br>
 *
 * <br> <b>Invariant:</b> type!=EMPTY => sub.mult==0
 * <br> <b>Invariant:</b> type!=EMPTY => vars.size()>0
 */

public final class ExprQuant extends Expr {

    /** The operator (ALL, NO, LONE, ONE, SOME, SUM, or COMPREHENSION) */
    public final Op op;

    /** The unmodifiable list of variables. */
    public final ConstList<ExprVar> vars;

    /** The unmodifiable list of variables. */
    public final ConstList<Decl> decls;
    
    /** The body of the quantified expression. */
    public final Expr sub;

    /** Caches the span() result. */
    private Pos span=null;

    //=============================================================================================================//

    /** {@inheritDoc} */
    @Override public Pos span() {
        Pos p=span;
        if (p==null) {
            p=pos.merge(closingBracket).merge(sub.span());
            // We intentionally do NOT merge the VAR's position into the span.
            // That allows us to control the highlighting of this component
            // simply by deciding this.pos and this.closingBracket
            span=p;
        }
        return p;
    }

    //=============================================================================================================//

    /** {@inheritDoc} */
    @Override public void toString(StringBuilder out, int indent, boolean newline) {
            
    	for(int i=0; i<indent && newline; i++) { out.append(' '); }
            
        if (op!=Op.COMPREHENSION) 
        	out.append('(').append(op).append(' '); 
        else 
        	out.append('{');

        String varlist = "";
        
        for(Decl d:decls) {
        	if (varlist.length() != 0) 
        		varlist += ", "; 
        	varlist += d.toString();
        }
 
        out.append(varlist);
        out.append(" | ");
        sub.toString(out, indent + 2, false);       

        if (op!=Op.COMPREHENSION) 
        	out.append(')'); 
        else 
        	out.append('}');
        
    }

    //=============================================================================================================//

    /** Constructs a new quantified expression. */
    private ExprQuant
        (Pos pos, Pos closingBracket, Op op, Type type, ConstList<Decl> decls, Expr sub, long weight, JoinableList<Err> errs) {
        super(pos, closingBracket, sub.ambiguous, type, 0, weight, errs);
        this.op=op;
        this.vars=null;
        this.decls=decls;
        this.sub=sub;
    }
    

    //=============================================================================================================//

    /** This class contains all possible quantification operators. */
    public enum Op {
        /** all  a,b:x | formula       */  ALL("all"),
        /** no   a,b:x | formula       */  NO("no"),
        /** lone a,b:x | formula       */  LONE("lone"),
        /** one  a,b:x | formula       */  ONE("one"),
        /** some a,b:x | formula       */  SOME("some"),
        /** sum  a,b:x | intExpression */  SUM("sum"),
        /** { a,b:x | formula }        */  COMPREHENSION("comprehension");

        /** The constructor. */
        private Op(String label) {this.label=label;}

        /** The human readable label for this operator. */
        private final String label;

        /**
         * Constructs a quantification expression with "this" as the operator.
         *
         * @param pos - the position of the "quantifier" in the source file (or null if unknown)
         * @param closingBracket - the position of the "closing bracket" in the source file (or null if unknown)
         * @param vars - the list of variables (each must be a variable over a set or relation)
         * @param sub - the body of the expression
         */
        public final Expr make(Pos pos, Pos closingBracket, List<Decl> vars, Expr sub) {
        	        	
        	return new ExprQuant(pos, closingBracket, this, EMPTY, ConstList.make(vars), sub, sub.weight, emptyListOfErrors);
        }

        /** Returns the human readable label for this operator */
        @Override public final String toString() { return label; }
    }

    //=============================================================================================================//

    /** {@inheritDoc} */
    public int getDepth() {
        int max = sub.getDepth();
        for(Expr x: vars) { int tmp=x.getDepth(); if (max<tmp) max=tmp; }
        return 1 + max;
    }

    /** {@inheritDoc} */
    @Override final<T> T accept(VisitReturn<T> visitor) throws Err { return visitor.visit(this); }
}
